Inference at * 
Iof proof for Lemma nth tl append:


  T:Type, as, bs:(T List). nth_tl(||as||;as @ bs) ~ bs 

latex

 by ((InductionOnList) 
CollapseTHEN (Reduce 0)) 

latex

C1: 

C1: 1. T : Type
C1: 2. T List
C1:   bs:(T List). bs ~ bs
C2: 

C2: 1. T : Type
C2: 2. T List
C2: 3. u : T
C2: 4. v : T List
C2: 5. bs:(T List). nth_tl(||v||;v @ bs) ~ bs
C2:   bs:(T List). nth_tl(||v||+1;[u / (v @ bs)]) ~ bs
C.

Definitions

x:A. B(x), s ~ t, x:AB(x), Type, s = t, type List, t  T, i z j, i <z j